perm filename FRAME.BNF[BNF,JRA] blob
sn#042357 filedate 1973-05-15 generic text, type T, neo UTF8
00100 <AXIOM> ::=<NAME><ASSUM><DRECUR><INEQ><BODY>
00200 =>(DEFPROP NAME BODY THEOREM)
00300 <NAME>::= <ID> =>*
00400
00500 <ASSUM>::= T =>T
00600 ::=NIL => NIL
00700
00800 <DRECUR> ::= T =>T
00900 ::= NIL => NIL
01000
01100 <INEQ> ::= NIL =>NIL
01200 ::=(<INARGS> =>*
01300
01400 <INARGS> ::= <INARG>,<INARGS> =>(INARG . INARGS)
01500 ::= <INARG>) =>(INARG)
01600
01700 <INARG> ::= X =>X
01800 ::= ⊗ =>⊗
01900
02000 <BODY> ::= <PRECOND><POSTCOND> =>(PRECOND . POSTCOND)
02100
02200 <PRECOND> ::= <PREPRED>;<PRECOND> =>(PREPRED . PRECOND)
02300 ::= ; =>((THSETQ(THV DBLITS)(CONS(CDAR CT)(THV DBLITS)))
02350 (COND((EQ(QUOTE IF)(CADAR CT))(ELSECLAUSE))(T(THSETQ CT (CDR CT)
02375 T T))))
02400
02500 <PREPRED> ::= <PRED> =>*
02600
02700 <PRED> ::= <NOT> <LIT> =>*
02800 ::= <LIT> =>*
02900
03000 <LIT> ::= <PREDLET><ITMLST> =>(PREDLET . ITMLST)
03100
03200 <ITMLST> ::= (<ITMS> =>*
03300
03400 <ITMS> ::= <TM2><ITMS> =>(TM2 . ITMS)
03500 ::= <TM>) =>(TM)
03600
03700 <TM2> ::= <TM>, =>*
03800
03900 <TM> ::= <IVAR> =>(THV IVAR)
04000 ::=<PREFN><ITMLST> =>(PREFN . ITMLST)
04100 ::= <PREFN> =>(PREFN)
04200
04300 <POSTCOND> ::= <POSTPRED>;<POSTCOND> =>(POSTPRED . POSTCOND)
04400 ::= ;=>NIL
04500 <POSTPRED> ::= <PRED> => *
04600
06000 <IVAR> ::= <ID> =>*
06100 <PREFN> ::= <ID> =>*
06200 <PREDLET> ::= <ID> =>*
06300
06350 <NOT> ::= ¬ => ¬
06400 END